\begin{tabbing}
1. $T$ : Type
\\[0ex]2. $n$ : $\mathbb{Z}$
\\[0ex]3. 0 $<$ $n$
\\[0ex]4. \=$\forall$$m$:$\mathbb{N}$, $b$:$T$, $c$:(\{0..(($n$ {-} 1)+$m$)$^{-}$\}$\rightarrow$$T$$\rightarrow$$T$).\+
\\[0ex]primrec(($n$ {-} 1)+$m$;$b$;$c$) = primrec($n$ {-} 1;primrec($m$;$b$;$c$);$\lambda$$i$,$t$. $c$($i$+$m$,$t$))
\-\\[0ex]5. $m$ : $\mathbb{N}$
\\[0ex]6. $b$ : $T$
\\[0ex]7. $c$ : \{0..($n$+$m$)$^{-}$\}$\rightarrow$$T$$\rightarrow$$T$
\\[0ex]$\vdash$  primrec($n$+$m$;$b$;$c$) = primrec($n$;primrec($m$;$b$;$c$);$\lambda$$i$,$t$. $c$($i$+$m$,$t$))
\end{tabbing}